package utils;

import java.io.IOException;
import java.util.LinkedList;
import java.util.TreeSet;

import algebra.visitors.ProjectionQueryVisitorEvaluator;

import kb.DescriptionLogicsKB;

import datatableaux.Reason;

import utils.parser.*;
import utils.exception.SyntaxParsingException;
import entities.Assertion;
import entities.concept.AndConcept;
import entities.concept.Concept;
import entities.concept.DomainConceptEQ;
import entities.concept.ExistsConcept;
import entities.role.GeneralRolePath;
import entities.role.Role;
import entities.vocabulary.KBVocabulary;

public class Util {

	private static TreeSet<String> listOfConstantsInTbox = new TreeSet<String>();
	private static String[] listOfConstantsArray;
	private static int oldSize = 0;
	private static final Reason reasoner = new Reason(false);
	private static int counter = 0;
	
	public static Reason getReasoner(){
		return reasoner;
	}
	public static int getCounter(){
		return counter;
	}
	public static void addKBConstants(String s){
		listOfConstantsInTbox.add(s);
	}
	//test if K |= C-> D iff K |= a:(~ C or D) is unsat
//	public static boolean subsumes(Concept a, Concept b, TBox tb){
////		System.out.print("Computing: " + a + " [under] " + b + " => ");		
//		Concept c = new NotConcept(a);	
//		Concept consist = new OrConcept(b, c);
////		Completion comp = new Completion(consist, tb);		
////		boolean res = !comp.isSatisfiable();
//		boolean res = reasoner.subsumes(consist, tb);
//		counter += 1;
////		System.out.println(res);
//		return res;
//	}
	
	//test if T |= a under b, as T and i:a |= i:b
	
	
	public static boolean subsumes(Concept lhs, Concept rhs, DescriptionLogicsKB kb) {
		Reason res = new Reason(false);
		return res.TBoxSubsumptionCheck(lhs, rhs, kb);
	}
	
	public static boolean assertionCheck(Assertion lhs, Assertion rhs, DescriptionLogicsKB kb){
		Reason res = new Reason(false);
		return res.ABoxUnionAssertionEntailAssertionCheck(lhs, rhs, kb);
	}
	
	public static Concept parseConcept(String s) {
		Tokenizer t = new Tokenizer(s);
        LinkedList<String> list = new LinkedList<String>();
		while(t.hasNextToken()) {
			String st = null;
			try {
				st = t.nextToken();
			} catch (IOException e) {
				e.printStackTrace();
			}
			list.add(st);
		}
		
		//System.out.println("Concept: " + s);
//		return null;
		Concept c = null;
		try {
			c = Parser.conParser(list);
		} catch (SyntaxParsingException e) {
			e.printStackTrace();
		}
		
		return c;
	}

	public static TreeSet<String> getListOfConstantsInTbox(){
		return listOfConstantsInTbox;
	}
	
	public static Concept parseConceptFromGeneralRolePath(GeneralRolePath grp, Concept c){
		if(grp == null || grp.length() == 0){
			return c;
		}
		Concept rc = c;
		for (int i = grp.length() - 1; i >= 0; i--) {
			Object item = grp.getContent().get(i);
			if(item instanceof Role){
				rc = new ExistsConcept((Role) item, rc);
			}else if(item instanceof Concept){
				boolean convert = false;
				if(ProjectionQueryVisitorEvaluator.allowMissingFeaturePatching){
					if(item instanceof DomainConceptEQ){
						String s = (String) ((DomainConceptEQ<?, ?>) item).getRealValue();
						if(s.equals(KBVocabulary.FeatureValueMissingPatch)){
							convert =true;
						}
					}
				}
				if(convert){
					//top and RC = RC
//					rc = new AndConcept(rc, KBVocabulary.CONCEPT_TOP);
//					System.out.println("converted:"+rc);
				}
				else{
					rc = new AndConcept(rc, (Concept)item);
				}
				
			}
		}
		return rc;
	}
	
//	public static Concept parseConceptFromRolePath(RolePath rp, Concept c) {
//		if (rp == null) {
//			return c;
//		}
//		if(rp.length() == 0){
//			if(rp.getConcept() == null){
//				return c;
//			}else{
//				return new AndConcept(rp.getConcept(), c);
//			}
//		}
//		// Convert a general role path to an existential concept
//		//String[] roles = rp.split(Projection.ROLE_PATH_DELIM);
//		Concept con = c;
//		if(rp.getConcept() != null){
//			con = new AndConcept(con, rp.getConcept());
//		}
//		for (int i = rp.length() - 1; i >= 0; i--) {
//			con = new ExistsConcept(rp.getRoles().get(i), con);
//		}
//		//System.out.println("parsed for "+c+","+rp +" to "+con);
//		return con;
//	}

	public static String[] getConstants() {
		if (oldSize != listOfConstantsInTbox.size() || listOfConstantsArray == null) {
			oldSize = listOfConstantsInTbox.size();
			listOfConstantsArray = new String[oldSize];
			listOfConstantsArray = listOfConstantsInTbox.toArray(listOfConstantsArray);
		}
		return listOfConstantsArray.clone();
	}

	

}
